T:Type, l1,l2:(T List), x:T. iseg(T; l1; l2)  (x  l1)  (x  l2) 

latex

Definitions	x:A. B(x), False, A, A  B, A c B, (x  l), P  Q, x:A. B(x), prop{i:l}, t  T,
Lemmas	select wf, nat wf, length wf1, le wf, l member wf, iseg wf